ds:x:Id fp Type, da:k:Knd fp Type, upd:update-spec(ds;da). update-spec-decl(upd;ds)  Prop 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, update-spec(ds;da), x.A(x), Top, x:AB(x), IdDeq, x  dom(f), b, Prop, update-spec-vars(upd), (x  l), P  Q, update-spec-decl(upd;ds)
Lemmas	l member wf, update-spec-vars wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, update-spec wf, Knd wf, fpf wf, Id wf